We consider quantitative extensions of the alternating-time temporal logicsATL/ATLs called quantitative alternating-time temporal logics (QATL/QATLs) inwhich the value of a counter can be compared to constants using equality,inequality and modulo constraints. We interpret these logics in one-countergame models which are infinite duration games played on finite control graphswhere each transition can increase or decrease the value of an unboundedcounter. That is, the state-space of these games are, generally, infinite. Weconsider the model-checking problem of the logics QATL and QATLs on one-countergame models with VASS semantics for which we develop algorithms and providematching lower bounds. Our algorithms are based on reductions of themodel-checking problems to model-checking games. This approach makes it quitesimple for us to deal with extensions of the logical languages as well as theinfinite state spaces. The framework generalizes on one hand qualitativeproblems such as ATL/ATLs model-checking of finite-state systems,model-checking of the branching-time temporal logics CTL and CTLs onone-counter processes and the realizability problem of LTL specifications. Onthe other hand the model-checking problem for QATL/QATLs generalizesquantitative problems such as the fixed-initial credit problem for energy games(in the case of QATL) and energy parity games (in the case of QATLs). Ourresults are positive as we show that the generalizations are not too costlywith respect to complexity. As a byproduct we obtain new results on thecomplexity of model-checking CTLs in one-counter processes and show thatdeciding the winner in one-counter games with LTL objectives is2ExpSpace-complete.
展开▼
